Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    first(0,X)  → nil
2:    first(s(X),cons(Y,Z))  → cons(Y,n__first(X,activate(Z)))
3:    from(X)  → cons(X,n__from(s(X)))
4:    first(X1,X2)  → n__first(X1,X2)
5:    from(X)  → n__from(X)
6:    activate(n__first(X1,X2))  → first(X1,X2)
7:    activate(n__from(X))  → from(X)
8:    activate(X)  → X
There are 3 dependency pairs:
9:    FIRST(s(X),cons(Y,Z))  → ACTIVATE(Z)
10:    ACTIVATE(n__first(X1,X2))  → FIRST(X1,X2)
11:    ACTIVATE(n__from(X))  → FROM(X)
The approximated dependency graph contains one SCC: {9,10}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 3, 2006